Termination check: handle recursion through proof trees and add recursive types check by Lysxia · Pull Request #2006 · creusot-rs/creusot

Lysxia · 2026-03-26T13:33:42Z

Handle recursion through proof trees (the original examples of Remaining unsoundness in the termination check #1232).
Termination checking of impl methods must happen under bounds of the original trait method declaration (see this comment from that same issue).
Add recursive types check:
- Types can only recurse in "strictly positive" positions.
- Recursive associated types are rejected (this also makes use of the new support for proof trees).
- Recursive traits are rejected (detecting additional counterexamples in Remaining unsoundness in the termination check #1232).
New attributes
- #[trusted(ghost)] (more fine grained than #[trusted] #[check(ghost)], i.e., it still enables Coma translation of program functions)
- #[trusted(terminates)] (idem, and can also be used on types)
- #[trusted(positive(T, U))] to postulate "strictly positive" type arguments (can also be used in extern_spec!)
Guide: expanded the Termination chapter with more details, recording the counterexamples found in Remaining unsoundness in the termination check #1232.

Some related things that are not handled in this PR:

There remains a recursion check in the translation pass, which may reject types that pass the new recursive type check (see the commented out example in the guide).
We'd like to use the new trait solver to better handle ambiguity, but AFAICT this only happens when a bound overlaps with an impl, in which case we should be able to pick the bound and do nothing more, which happens to match the current behavior, so we don't have a pressing reason to use the more "proper" entry point to the trait solver (Use new trait solver API to avoid ambiguity errors #1671)
We'd like to better detect empty recursive types (struct Never(Box<Never>), Reject empty types before Why3 rejects them. #881)

Finally, I put traits in the same dependency graph as types, but there are currently no edges between traits and types. When checking traits, I only find dependencies to other traits in trait bounds (for instance, trait Tr0 where T1: Tr2<T3> has an edge Tr0 -> Tr2, and T1 and T3 are ignored). And when checking types, there are no edges due to bounds (in struct T<A: Tr>(A), Tr is ignored; but we will track dependencies to trait impls whenever T is instantiated) or trait objects dyn Tr (because they are unsupported). Can you find a counterexample where that breaks soundness?

jhjourdan · 2026-03-26T13:49:02Z

Ok, many thanks for that!

There is a lot of things to review, and I need to think about this, because there is a lot of potential for unsoundness.

Lysxia · 2026-03-27T18:32:57Z

there are currently no edges between traits and types

I came up with an argument for that. You can split every trait in two: its associated types on one side, and its methods and supertrait constraints on the other side. Once associated type declarations are viewed as standalone constructs, they depend on nothing. That's why there is no need to track dependencies between ADTs and associated type declarations (which are different from associated trait instances, for which I do track dependencies).

The only remaining dependencies from types to traits are via trait objects, which are basically not supported at the moment.

jhjourdan · 2026-03-28T11:28:58Z

Cannot associated types depend on associated types of subtraits?

Lysxia · 2026-03-28T11:40:02Z

I don't see how.

Another way to think about it is that associated types are like extra type parameters (as they would actually be in Rocq), with differences only relevant to type inference.

trait Tr {
   type A;
}

struct S<T: Tr>(T::A);

// is like

trait Tr<A> {
}

struct S<A, T: Tr<A>>(A);

jhjourdan

That's very good work, which solves many difficult problems in Creusot. Thanks.

Why did you not use the proof tree API from rustc, finally?

Do we agree that this does not fully addresses #1232, since it does not solve the problem with default functions?

jhjourdan · 2026-05-04T14:24:20Z

+
+The attribute `#[trusted(positive(T))]` can be used on a `struct` or `enum`
+to postulate that certain arguments are strictly positive.
+


Suggested change

The attribute `#[trusted(positive(T))]` can be used on a `struct` or `enum`

to postulate that certain arguments are strictly positive. Note that Creusot

does not check anything about this annotation (hence the use of the

`#[trusted` attribute). It is the user's responsibility to not use this annotation

on non-strictly positive types.

jhjourdan · 2026-05-04T14:29:19Z

+```
+
+If this were accepted by Creusot, the associated type `Dummy::A` would be equivalent to
+`Mapping<Dummy::A, bool>`, which would be unsound as explained in a [previous counterexample](#counterexample).


The link is ambiguous.

jhjourdan · 2026-05-05T22:00:56Z

 /// Cell over predicates
 ///
 /// A wrapper around `std::cell::Cell` that allows predicates to be used to specify the contents of the cell.
+#[trusted(positive(T))]


I'm really not sure for this one. A PredCell<T> is essentially a predicate over T, so it is essentially negative. I really suspect one can build a contradiction using this.

jhjourdan · 2026-05-05T22:56:01Z

+
+impl ProgramPurity {
+    pub fn is_ghost(self) -> bool {
+        self == ProgramPurity::Ghost


Suggested change

self == ProgramPurity::Ghost

self >= ProgramPurity::Ghost

(More robust wrt. maintainance.)

jhjourdan · 2026-05-06T09:45:37Z

+    }
+}
+
+pub fn select_method<'tcx>(


Suggested change

pub fn select_method<'tcx>(

fn select_method<'tcx>(

jhjourdan · 2026-05-07T15:44:17Z

    s.valid()
 }
+
+fn as_predicates<'tcx>(


Suggested change

fn as_predicates<'tcx>(

fn trait_refs_of_clauses<'tcx>(

jhjourdan · 2026-05-07T16:33:49Z

+            // Some bounds can be trait aliases and we skip them.
+            // The implied bounds should already appear separately.


I've never understood whether this is indeed the case. Do we have a test for that?

(I know that this is unrelated to this PR, but still, that's good to check that now.)

jhjourdan · 2026-05-07T16:56:37Z

+        let ImplSelection::Found(source) = select_trait_impl(tcx, typing_env, trait_ref) else {
+            continue;
+        };
+        let ImplSource::UserDefined(source) = source else { continue };


So in the end you decided to not use the new ProofTree API?

This seems good like this, apart from the fact that I'm afraid that we will miss some dependencies due to builtin impls.

For now, I don't this this should be a problem, because Creusot does not handle these builtin impls anyway (see #2094). But with this implementation technique, we are missing dependencies introduced by impls for Clone.

For a list of them (for Clone only), see instantiate_constituent_tys_for_copy_clone_trait in rustc source. I have not found any other builtin trait that could cause this issue (but there might be some, including in the future).

jhjourdan · 2026-05-07T17:06:32Z

+    let args = tcx.mk_args_from_iter(
+        trait_ref.args.iter().chain(trait_item_args.iter().skip(trait_ref.args.len())),
+    );


That's exactly rebase_onto.

jhjourdan · 2026-05-07T17:12:08Z

+    tgt: graph::NodeIndex,
+    path: &mut Vec<graph::NodeIndex>,
+    visited: &mut HashSet<graph::NodeIndex>,
+) -> Result<(), ()> {


It's a bit weird to use Result for that, because the error case is actually not an error, it is what we are searching for.

Lysxia force-pushed the termination-tree branch 2 times, most recently from 4718c2c to e032a4d Compare March 26, 2026 14:06

Lysxia mentioned this pull request Apr 9, 2026

Streamline tracking of dependencies #2026

Open

Lysxia force-pushed the termination-tree branch 5 times, most recently from b449dfd to 64422e4 Compare April 23, 2026 14:18

Lysxia force-pushed the termination-tree branch 3 times, most recently from 6603c32 to 7b072b6 Compare April 29, 2026 08:46

Lysxia added 4 commits April 29, 2026 11:24

Refactor resolve_item to separate the handling of traits from methods

a90d17f

Handle proof trees in termination check

24b4abc

Add recursive type check

805ecc8

guide: Add more details about termination check

2d02416

Lysxia force-pushed the termination-tree branch from 7b072b6 to 2d02416 Compare April 29, 2026 09:25

jhjourdan approved these changes May 7, 2026

View reviewed changes


		The attribute `#[trusted(positive(T))]` can be used on a `struct` or `enum`
		to postulate that certain arguments are strictly positive.

+The attribute `#[trusted(positive(T))]` can be used on a `struct` or `enum`
+to postulate that certain arguments are strictly positive. Note that Creusot
+does not check anything about this annotation (hence the use of the
+`#[trusted` attribute). It is the user's responsibility to not use this annotation
+on non-strictly positive types.

		// Some bounds can be trait aliases and we skip them.
		// The implied bounds should already appear separately.

Conversation

Lysxia commented Mar 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jhjourdan commented Mar 26, 2026

Uh oh!

Lysxia commented Mar 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jhjourdan commented Mar 28, 2026

Uh oh!

Lysxia commented Mar 28, 2026

Uh oh!

jhjourdan left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Lysxia commented Mar 26, 2026 •

edited

Loading

Lysxia commented Mar 27, 2026 •

edited

Loading